/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package simhya.modelchecking.mtl;

/**
 *
 * @author Luca
 */
public class MTLand  extends MTLnode {
    
    public MTLand(MTLnode left, MTLnode right) {
        super();
        super.setChildren(left,right);
        left.setParent(this);
        right.setParent(this);
    }
    
    @Override
    public String toFormulaTree(int depth) {
        String s = "";
        for (int i=0;i<depth;i++)
            s += "   ";
        s += "AND\n";
        return s + super.toFormulaTree(depth);
    }
    
    
    @Override
    ParametricInterval setExplorableTopNodes(String parameter) {
        if (this.isTopNode) {
           ParametricInterval l = left.setExplorableTopNodes(parameter);
           ParametricInterval r = right.setExplorableTopNodes(parameter);
           if (!l.equals(r))
               return null;
           else return l;
        } else return null;
    }
    
    @Override
    void labelingFormulaPointwiseSemantics(double[] deltaTimes) {
        for (int i=0;i<this.traceLength;i++)
            this.truthValue[i] = left.truthValue[i] && right.truthValue[i];
    }

    @Override
    void labelingTopFormulaPointwiseSemantics(double[] deltaTimes, boolean varyInterval, boolean varyRightBound, int points) {
        if (left.truthValue.length == 1) {
            if (right.truthValue.length == 1)
                //case 1 - 1
                this.truthValue[0] = left.truthValue[0] && right.truthValue[0];
            else
                //case 1 - many
                for (int i=0;i<points;i++)
                    this.truthValue[i] = left.truthValue[0] && right.truthValue[i];
        } else {
            if (right.truthValue.length == 1)
                //case  many - 1
                for (int i=0;i<points;i++)
                    this.truthValue[i] = left.truthValue[i] && right.truthValue[0];
            else
                //case  many - many
                for (int i=0;i<points;i++)
                    this.truthValue[i] = left.truthValue[i] && right.truthValue[i];
        }    
    }
    
}
